% To run load a Prolog system (e.g. sicstus, swi, yap) and consult:
% ?- [priolog,qsort].
%
% then query for, e.g.:
%
% hyp(qsort([4,2,1,7],[1,2,4,7]), H, A, P)
% findall(H, hyp(qsort([4,2,1,7],[1,2,4,7]), H, A, P), L), length(L, N)
% :-start, findall(H, hyp(qsort([3,2,1,0],[0,1,2,3]), H, A, P), L), length(L, N),write(L),nl,write(N),nl, statistics.

qsort([], []).

% qsort([H|T], S):-
%   part(H, T, SH, BH),
%   qsort(SH, SSH),
%   qsort(BH, SBH),
%   append(SSH, [H|SBH], S).

append([], L, L).
append([H|T], L, [H|R]):-
  append(T, L, R).

part(_, [], [], []).
part(A, [H|T], [H|P], S) :- 
  A >= H,
  part(A, T, P, S).
part(A, [H|T], P, [H|S]) :- 
  A < H,
  part(A, T, P, S).

:-set(maximum_literals_in_hypothesis, 6).

:-modeh(qsort(+list,-list)).
:-modeb(+list=[-any|-list]). %:-modet(l2ht(+list/[H|T], -any/H, -list/T)).
:-modeb(part(+any,+list,-list,-list)).
:-modeb(2, qsort(+list,-list)).
:-modeb(-list=[+any|+list]). %:-modet(ht2l(+any/H, +list/T, -list/[H|T])).
:-modeb(append(+list,+list,-list)).


example(qsort([],[]), 1).
example(qsort([0], [0]), 1).
example(qsort([1], [1]), 1).
example(qsort([2], [2]), 1).
example(qsort([3], [3]), 1).
example(qsort([0,1], [0,1]), 1).
example(qsort([0,2], [0,2]), 1).
example(qsort([0,3], [0,3]), 1).
example(qsort([1,0], [0,1]), 1).
example(qsort([1,2], [1,2]), 1).
example(qsort([1,3], [1,3]), 1).
example(qsort([2,0], [0,2]), 1).
example(qsort([2,1], [1,2]), 1).
example(qsort([2,3], [2,3]), 1).
example(qsort([3,0], [0,3]), 1).
example(qsort([3,1], [1,3]), 1).
example(qsort([3,2], [2,3]), 1).
example(qsort([0,1,2], [0,1,2]), 1).
example(qsort([0,1,3], [0,1,3]), 1).
example(qsort([0,2,1], [0,1,2]), 1).
example(qsort([0,2,3], [0,2,3]), 1).
example(qsort([0,3,1], [0,1,3]), 1).
example(qsort([0,3,2], [0,2,3]), 1).
example(qsort([1,0,2], [0,1,2]), 1).
example(qsort([1,0,3], [0,1,3]), 1).
example(qsort([1,2,0], [0,1,2]), 1).
example(qsort([1,2,3], [1,2,3]), 1).
example(qsort([1,3,0], [0,1,3]), 1).
example(qsort([1,3,2], [1,2,3]), 1).
example(qsort([2,0,1], [0,1,2]), 1).
example(qsort([2,0,3], [0,2,3]), 1).
example(qsort([2,1,0], [0,1,2]), 1).
example(qsort([2,1,3], [1,2,3]), 1).
example(qsort([2,3,0], [0,2,3]), 1).
example(qsort([2,3,1], [1,2,3]), 1).
example(qsort([3,0,1], [0,1,3]), 1).
example(qsort([3,0,2], [0,2,3]), 1).
example(qsort([3,1,0], [0,1,3]), 1).
example(qsort([3,1,2], [1,2,3]), 1).
example(qsort([3,2,0], [0,2,3]), 1).
example(qsort([3,2,1], [1,2,3]), 1).
example(qsort([3,2,0,1], [0,1,2,3]), 1).
example(qsort([3,1,2,0], [0,1,2,3]), 1).
example(qsort([3,1,0,2], [0,1,2,3]), 1).
example(qsort([3,0,2,1], [0,1,2,3]), 1).
example(qsort([3,0,1,2], [0,1,2,3]), 1).
example(qsort([2,3,1,0], [0,1,2,3]), 1).
example(qsort([2,3,0,1], [0,1,2,3]), 1).
example(qsort([2,1,3,0], [0,1,2,3]), 1).
example(qsort([2,1,0,3], [0,1,2,3]), 1).
example(qsort([2,0,3,1], [0,1,2,3]), 1).
example(qsort([2,0,1,3], [0,1,2,3]), 1).
example(qsort([1,3,2,0], [0,1,2,3]), 1).
example(qsort([1,3,0,2], [0,1,2,3]), 1).
example(qsort([1,2,3,0], [0,1,2,3]), 1).
example(qsort([1,2,0,3], [0,1,2,3]), 1).
example(qsort([1,0,3,2], [0,1,2,3]), 1).
example(qsort([1,0,2,3], [0,1,2,3]), 1).
example(qsort([0,3,2,1], [0,1,2,3]), 1).
example(qsort([0,3,1,2], [0,1,2,3]), 1).
example(qsort([0,2,1,3], [0,1,2,3]), 1).
example(qsort([0,2,3,1], [0,1,2,3]), 1).
example(qsort([0,1,3,2], [0,1,2,3]), 1).
example(qsort([0,1,2,3], [0,1,2,3]), 1).


example(qsort([3,2,1,0],[]), -1).
example(qsort([0,2,1],[0,2,1]), -1).
example(qsort([0,2,1],[0,1]), -1).
example(qsort([1,0,2],[2,0,1]), -1).
example(qsort([1,0,2],[2,1,0]), -1).
example(qsort([1,2,0],[1,0,2]), -1).
example(qsort([0,2,1],[2,1,0]), -1).
example(qsort([2,1,0],[2,1,0]), -1).
example(qsort([2,0,1],[2,1,0]), -1).
example(qsort([2,1],[1]), -1).
example(qsort([1],[2]), -1).
example(qsort([0,1,2],[1,0,2]), -1).
example(qsort([0,1],[1,0,1]), -1).

%:-theory_builder:start.
%hyp_builder:hyp(qsort([5,4,1,3],[1,3,4,5]),H,P)